#!/usr/bin/python
# -*- coding: utf8 -*-

from pyparsing import Literal, Regex, Keyword

from expresion import Expresion, Exp, TypeException, TipoExp, Id, makeSintaxis
from functions import Func, Abstraccion
from let import Let

from lenguaje import Extension

class Fix(Expresion):
    
    def __init__(self, tok):
        """
        La expresion fix esta compuesta a su vez por una espresion.
        """
        self.exp = tok[0]
    
    def reducir(self):
        # M -> M'
        # --------------
        # fix(M) -> fix(M')
        expRed = self.exp.reducir()
        
        # --------------------
        # fix(\\X:sigma.M) -> M{ X <- fix(\\X:sigma.M)}
        res = expRed.expresion.sustituir(expRed.var, Fix([expRed]))
        
        return res.reducir()
    
    
    def tipar(self, namespace):
        """
        gamma |> M : sigma -> sigma
        ----------------------------------
        gama |> fix (M) : sigma
        """
        tipoExp = self.exp.tipar(namespace)
        #gamma |> M : sigma -> sigma
        if isinstance(tipoExp, Func):
            if tipoExp.dominio == tipoExp.imagen:
                # gama |> fix (M) : sigma
                return tipoExp.dominio
            else:
                raise TypeException("El dominio de %s es %s y su imagen deberia ser igual, pero es %s" % (self.exp, tipoExp.dominio, tipoExp.imagen))
        else:
            raise TypeException("El termino %s debe ser una abstraccion para estar en un fix" % self.exp)
    
    def sustituir(self, var, expresion):
        """
        fix(E) {X <- T} --> fix(E {X <- T})
        """
        return Fix([self.exp.sustituir(var, expresion)])
    
    @classmethod
    def sintaxis(cls):
        return makeSintaxis("fix(", Exp, ')')
    
    def __str__(self):
        return "fix(%s)" % self.exp
    
    
class LetRec(Expresion):
    
    def __init__(self, toks):
        """
        letrec esta compuesto por una variable, el tipo de esa variable
        un termino asignado a esa variable, y una expresion en donde se reemplazara
        cada aparicion de la varible por el termino asociado.
        """
        var, tipoVar, exp1, exp2 = toks
        self.var = var
        self.tipoVar = tipoVar
        self.exp1 = exp1
        self.exp2 = exp2
    
    
    # Para definir letRec usamos que:
    #    letrec f : sigma = \\x :alpha.M in N
    #    es equivalente a
    #    let f = fix(\f : sigma -> sigma.\\x:alpha.M) in N
    # Usando esto para tipar y reducir un letRec creamos su expresion equivalente y aplicamos sus reglas
    
    
    def reducir(self):
        expAux = Let([self.var, Fix([Abstraccion([self.var, Func([self.tipoVar, self.tipoVar]),self.exp1])]), self.exp2])
        return expAux.reducir()
        
    def tipar(self, namespace):
        nam2 = dict(namespace)
        nam2[self.var] = self.tipoVar
        tipo = self.exp1.tipar(nam2)
        expAux = Let([self.var, Fix([Abstraccion([self.var, self.tipoVar, self.exp1])]), self.exp2])
        return expAux.tipar(namespace)
    
    def sustituir(self,var,expresion):
        expAux = Let([self.var, Fix([Abstraccion([self.var, Func([self.tipoVar, self.tipoVar]), self.exp1])]), self.exp2])
        return expAux.sustituir(var, expresion)
            
    @classmethod
    def sintaxis(cls):
        return makeSintaxis("letrec", Id ,':', TipoExp,'=',Exp, 'in',Exp)
    
    def __str__(self):
        return "letrec %s:%s = %s in %s" % (self.var, self.tipoVar, self.exp1, self.exp2)
    

extensionLetRec = Extension("LetRec", expresiones=[Fix, LetRec])
